<!DOCTYPE html>
<!--
     SPDX-License-Identifier: CC-BY-SA-4.0
     SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
-->
<!-- Page last generated 2025-02-20 03:16:15 +0000 -->
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta http-equiv="X-UA-Compatible" content="IE=edge">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>MCS | seL4 docs</title>

    <!-- Our stylesheet and theme stylesheet.  Contains bootstrap. -->
    <link rel="stylesheet" href="/assets/css/style.css" type="text/css">
    <!-- Font awesome -->
    <link href="https://use.fontawesome.com/releases/v5.0.8/css/all.css" rel="stylesheet">
    <link href="https://fonts.googleapis.com/css2?family=Roboto&display=swap" rel="stylesheet">
    <!-- Pygments syntax highlighting  -->
    <link rel="stylesheet" href="/assets/css/highlighting/trac.css" type="text/css">
    <link rel="icon" type="image/x-icon" href="/assets/favicon.ico"><script defer data-domain="docs.sel4.systems"
	    src="https://analytics.sel4.systems/js/script.js"></script></head>

  <body class="container-fluid">

    



<header>
  <ul class="row menu">
    <li class="col-xs-12 col-md-2" >
            <a href="https://sel4.systems" class="skip-icon">
              <img class="img-responsive" src="/assets/logo-text-white.svg" alt="seL4 logo" />
            </a>
    </li>
    <li class="col-xs-12 col-md-10 menu">
      <nav aria-label="Banner links">
        <h2><a href="/Resources" />Resources</h2>
        <h2><a href="/processes" />Contributing</a></h2>
        <h2><a href="/projects" />Projects</h2>
        <h2><a href="/Tutorials" />Tutorials</h2>
        <iframe title="DuckDuckGo search bar" src="https://duckduckgo.com/search.html?site=docs.sel4.systems&prefill=Search%20sel4.systems" style="overflow:hidden;margin-bottom:10px; padding:0;height:40px;float:right;border-width: 0px"></iframe>
      </nav>
    </li>
  </ul>
  <div class="clear"></div>
  
<div class="breadcrumbs bootstrap hidden-sm-down">
  <nav class="sel-breadcrumb" aria-label="Breadcrumb" >
    <ol class=" list-unstyled" vocab="http://schema.org/" typeof="BreadcrumbList">
      
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/">
              <span property="name"><b>seL4 Docs</b></span>
            </a>
            <meta property="position" content="1" />
        </li>
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/Tutorials/">
              <span property="name"><b>Tutorials</b></span>
            </a>
            <meta property="position" content="2" />
        </li>
      
        

        
          <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <span property="name">MCS</span>
            <meta property="position" content="3" /></li>
          
    </ol>
  </nav>
  <nav class="sel-version" aria-label="Current Versions">
    <ol class="list-unstyled">
      <li class="list-unstyled text-right" style="margin-left:auto; padding:0rem 0rem;">
        Current versions:</li>
      <li class="list-unstyled text-right">
      <a href="/releases/sel4/13.0.0"><b>seL4-13.0.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/microkit/1.4.1"><b>microkit-1.4.1</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/camkes/camkes-3.11.0"><b>camkes-3.11.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/capdl/0.3.0"><b>capDL-0.3.0</b></a></li>
      </ol>
  </nav>
  <div class='clear'></div>
</div>


</header>

    <main>
      <div class="row">
  <div class="hidden-xs col-sm-4 col-md-3 col-lg-2">
    

<div class="sidebar">
  <ul class="nav nav-sidebar tutorial-sidebar">
    <li class="nav-section">Getting started</li>
      <li><a href="/Tutorials/">Overview</a></li>
      <li><a href="/Tutorials/pathways">Tutorial pathways</a></li>
    <li class="nav-section">seL4</li>
      <li><a href="/Tutorials/setting-up">Setting up your machine</a></li>
      <li><a href="/Tutorials/get-the-tutorials">Getting the tutorials</a></li>
      <li><a href="/Tutorials/hello-world">Hello world</a></li>
      <li><a href="/Tutorials/capabilities">Capabilities</a></li>
      <li><a href="/Tutorials/untyped">Untyped</a></li>
      <li><a href="/Tutorials/mapping">Mapping</a></li>
      <li><a href="/Tutorials/threads">Threads</a></li>
      <li><a href="/Tutorials/ipc">IPC</a></li>
      <li><a href="/Tutorials/notifications">Notifications</a></li>
      <li><a href="/Tutorials/interrupts">Interrupts</a></li>
      <li><a href="/Tutorials/fault-handlers">Fault handling</a></li>
      <li><a href="/Tutorials/mcs">MCS extensions</a></li>
    <li class="nav-section">C Libraries</li>
      <li><a href="/Tutorials/libraries-1">Initialisation &amp; threading</a></li>
      <li><a href="/Tutorials/libraries-2">IPC</a></li>
      <li><a href="/Tutorials/libraries-3">Processes &amp; Elf loading</a></li>
      <li><a href="/Tutorials/libraries-4">Timer</a></li>
    <li class="nav-section">Microkit</li>
      <li><a href="https://trustworthy.systems/projects/microkit/tutorial/">Tutorial</a></li>
    <li class="nav-section">CAmkES</li>
      <li><a href="/Tutorials/hello-camkes-0">Hello CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-1">Introduction to CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-2">Events in CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-timer">CAmkES timer tutorial</a></li>
      <li><a href="/Tutorials/camkes-vm-linux">CAmkES VM</a></li>
      <li><a href="/Tutorials/camkes-vm-crossvm">CAmkES cross-VM connectors</a></li>
    <li class="nav-section">Rust</li>
      <li><a href="https://github.com/seL4/rust-sel4">GitHub</a></li>
    <li class="nav-section">Resources</li>
      <li><a href="https://sel4.systems/Info/Docs/seL4-manual-latest.pdf">seL4 Manual</a></li>
      <li><a href="/projects/sel4/api-doc.html">seL4 API reference</a></li>
      <li><a href="/Tutorials/how-to">How to: a quick solutions guide</a></li>
      <li><a href="/projects/sel4-tutorials/debugging-guide">Debugging guide</a></li>
      <li><a href="/Resources#contact">Help contacts</a></li>
  </ul>
</div>

  </div>
  <div class="content col-sm-8 col-md-6 col-lg-7 main">

    
<!--
  Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)

  SPDX-License-Identifier: BSD-2-Clause
-->

<h1 id="mcs-extensions">MCS Extensions</h1>

<p>This tutorial presents the features in the Mixed-Criticality System (MCS) extensions for seL4, which are currently undergoing
verification. For further context on the new features, please see the
<a href="https://trustworthy.systems/publications/csiro_full_text/Lyons_MAH_18.pdf">paper</a> or <a href="https://github.com/pingerino/phd/blob/master/phd.pdf">phd</a>
 which provides a comprehensive background on the changes.</p>

<p>Learn:</p>
<ol>
  <li>About the MCS new kernel API.</li>
  <li>How to create and configure scheduling contexts.</li>
  <li>The jargon <em>passive server</em>.</li>
  <li>How to spawn round-robin and periodic threads.</li>
</ol>

<h2 id="prerequisites">Prerequisites</h2>

<ol>
  <li><a href="/Tutorials/setting-up">Set up your machine</a></li>
  <li><a href="/Tutorials/hello-world">Hello world tutorial</a></li>
  <li><a href="/Tutorials/capabilities">Capabilities tutorial</a></li>
  <li><a href="/Tutorials/untyped">Untyped tutorial</a></li>
  <li><a href="/Tutorials/mapping">Mapping tutorial</a></li>
  <li><a href="/Tutorials/threads">Threads tutorial</a></li>
  <li><a href="/Tutorials/ipc">IPC tutorial</a></li>
  <li><a href="/Tutorials/notifications">Notifications tutorial</a></li>
  <li><a href="/Tutorials/interrupts">Interrupts tutorial</a></li>
  <li><a href="/Tutorials/fault-handlers">Fault handlers tutorial</a></li>
</ol>

<h2 id="initialising">Initialising</h2>

<p>Then initialise the tutorial:</p>

<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="c"># For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/get-the-tutorials</span>
<span class="c">#</span>
<span class="c"># Follow these instructions to initialise the tutorial</span>
<span class="c"># initialising the build directory with a tutorial exercise</span>
./init <span class="nt">--tut</span> mcs
<span class="c"># building the tutorial exercise</span>
<span class="nb">cd </span>mcs_build
ninja
</code></pre></div></div>

<details>
  <summary><em>Hint:</em> tutorial solutions</summary>
  <p><br />
All tutorials come with complete solutions. To get solutions run:</p>

  <div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="c"># For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/get-the-tutorials</span>
<span class="c">#</span>
<span class="c"># Follow these instructions to initialise the tutorial</span>
<span class="c"># initialising the build directory with a tutorial exercise</span>
./init <span class="nt">--solution</span> <span class="nt">--tut</span> mcs
<span class="c"># building the tutorial exercise</span>
<span class="nb">cd </span>mcs_build
ninja
</code></pre></div>  </div>

</details>

<h2 id="background">Background</h2>

<p>The MCS extensions provide capability-based access to CPU time, and provide mechanisms to limit the upper
bound of execution of a thread.</p>

<h3 id="scheduling-contexts">Scheduling Contexts</h3>

<p>Scheduling contexts are a new object type in the kernel, which contain scheduling parameters amoung other
accounting details. Most importantly, scheduling contexts contain a <em>budget</em> and a <em>period</em>, which
represent an upper bound on execution time allocated: the kernel will enforce that threads cannot execute
for more than <em>budget</em> microseconds out of <em>period</em> microseconds.</p>

<h3 id="schedcontrol">SchedControl</h3>

<p>Parameters for scheduling contexts are configured by invoking <code class="language-plaintext highlighter-rouge">seL4_SchedControl</code> capabilities, one of
which is provided per CPU. The invoked <code class="language-plaintext highlighter-rouge">seL4_SchedControl</code> determines which processing core that specific
scheduling context provides access to.</p>

<p>Scheduling contexts can be configured as <em>full</em> or <em>partial</em>. Full scheduling contexts have <code class="language-plaintext highlighter-rouge">budget ==
period</code> and grant access to 100% of CPU time. Partial scheduling contexts grant access to an upper bound of
 <code class="language-plaintext highlighter-rouge">budget/period</code> CPU time.</p>

<p>The code example below configures a
scheduling context with a budget and period both equal to 1000us. Because the budget and period are equal,
the scheduling context is treated as round-robin</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_SchedControl_Configure</span><span class="p">(</span><span class="n">sched_control</span><span class="p">,</span> <span class="n">sched_context</span><span class="p">,</span> <span class="n">US_IN_S</span><span class="p">,</span> <span class="n">US_IN_S</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="mi">0</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span> <span class="o">!=</span> <span class="n">seL4_NoError</span><span class="p">,</span> <span class="s">"Failed to configure schedcontext"</span><span class="p">);</span>
</code></pre></div></div>

<h3 id="schedcontext-binding">SchedContext Binding</h3>

<p>Thread control blocks (TCBs) must have a scheduling context configured with non-zero budget and period
 in order to be picked by the scheduler. This
can by invoking the scheduling context capability with the <code class="language-plaintext highlighter-rouge">seL4_SchedContext_Bind</code> invocation, or by
using <code class="language-plaintext highlighter-rouge">seL4_TCB_SetSchedParams</code>, which takes a scheduling context capability. Below is example code for
binding a TCB and a scheduling context.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_SchedContext_Bind</span><span class="p">(</span><span class="n">sched_context</span><span class="p">,</span> <span class="n">spinner_tcb</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span> <span class="o">!=</span> <span class="n">seL4_NoError</span><span class="p">,</span> <span class="s">"Failed to bind sched_context to round_robin_tcb"</span><span class="p">);</span>
</code></pre></div></div>

<p>TCB’s can only be bound to one scheduling context at a time, and vice versa. If a scheduling context has not
been configured with any time, then although the TCB has a scheduling context it will remain ineligible
for scheduling.</p>

<h3 id="bounding-execution">Bounding execution</h3>

<p>For partial scheduling contexts, an upper bound on execution is enforced by seL4 using the <em>sporadic server</em>
algorithm, which work by guaranteeing the <em>sliding window</em> constrain, meaning that during any period, the
budget cannot be exceeded. This is achieved by tracking the eligible budget in chunks called
<em>replenishments</em> (abbreviated to <code class="language-plaintext highlighter-rouge">refills</code> in the API for brevity). A replenishment is simply an amount
 of time, and a timestamp from which that time can be consumed. We explain this now through an example:</p>

<p>Consider a scheduling context with period <em>T</em> and budget <em>C</em>. Initially, the scheduling context has
a single replenishment of size <em>C</em> which is eligible to be used from time <em>t</em>.</p>

<p>The scheduling context is scheduled at time <em>t</em> and blocks at time <em>t + n</em>. A new replenishment is then scheduled
for time <em>t+T</em> for <em>n</em>. The existing replenishment is updated to <em>C - n</em>, subtracting the amount consumed.
For further details on the sporadic server algorithm, see the
<a href="https://dl.acm.org/citation.cfm?id=917665">original paper</a>.</p>

<p>If the replenishment data structure is full, replenishments are merged and the upper bound on execution is
reduced. For this reason, the bound on execution is configurable with the <code class="language-plaintext highlighter-rouge">extra_refills</code> parameter
on scheduling contexts. By default, scheduling contexts contain only two parameters, meaning if a
scheduling context is blocked, switched or preempted more than twice, the rest of the budget is forfeit until
the next period. <code class="language-plaintext highlighter-rouge">extra_refills</code> provides more replenishment data structures in a scheduling context. Note
that the higher the number of replenishments the more fragmentation of budget can occur, which will increase
scheduling overhead.</p>

<p><code class="language-plaintext highlighter-rouge">extra_refills</code> itself is bounded by the size of a scheduling context, which is itself configurable.
On scheduling context creation a size can be specified, and must be <code class="language-plaintext highlighter-rouge">&gt; seL4_MinSchedContextBits</code>. The
maximum number of extra refills that can fit into a specific scheduling context size can be calculated
with the function <code class="language-plaintext highlighter-rouge">seL4_MaxExtraRefills()</code> provided in <code class="language-plaintext highlighter-rouge">libsel4</code>.</p>

<p>Threads bound to scheduling contexts that do not have an available replenishment are placed into an ordered
queue of threads, and woken once their next replenishment is ready.</p>

<h3 id="scheduler">Scheduler</h3>

<p>The seL4 scheduler is largely unchanged: the highest priority, non-blocked thread with a configured
 scheduling context that has available budget is chosen by the scheduler to run.</p>

<h3 id="passive-servers">Passive servers</h3>

<p>The MCS extensions allow for RPC style servers to run on client TCBs’ scheduling contexts. This is achived by
unbinding the scheduling context once a server is blocked on an endpoint, rendering the server <em>passive</em>.
Caller scheduling contexts are donated to the server on <code class="language-plaintext highlighter-rouge">seL4_Call</code> and returned on <code class="language-plaintext highlighter-rouge">seL4_ReplyRecv</code>.</p>

<p>Passive servers can also receive scheduling contexts from their bound notification object, which is
achieved by binding a notification object using <code class="language-plaintext highlighter-rouge">seL4_SchedContext_Bind</code>.</p>

<h3 id="timeout-faults">Timeout faults</h3>

<p>Threads can register a timeout fault handler using <code class="language-plaintext highlighter-rouge">seL4_TCB_SetTimeoutEndpoint</code>. Timeout fault
handlers are optional and are raised when a thread’s replenishment expires <em>and</em> they have a valid handler
registered. The timeout fault message from the kernel contains the data word which can be used to identify the
scheduling context that the thread was using when the timeout fault occurred, and the amount of time
consumed by the thread since the last fault or <code class="language-plaintext highlighter-rouge">seL4_SchedContext_Consumed</code>.</p>

<h3 id="new-invocations">New invocations</h3>

<ul>
  <li><code class="language-plaintext highlighter-rouge">seL4_SchedContext_Bind</code> - bind a TCB or Notification capability to the invoked scheduling context.</li>
  <li><code class="language-plaintext highlighter-rouge">seL4_SchedContext_Unbind</code> - unbind any objects from the invoked scheduling context.</li>
  <li><code class="language-plaintext highlighter-rouge">seL4_SchedContext_UnbindObject</code>- unbind a specific object from the invoked scheduling context.</li>
  <li><code class="language-plaintext highlighter-rouge">seL4_SchedContext_YieldTo</code> - if the thread running on the invoked scheduling context is
schedulable, place it at the head of the scheduling queue for its priority. For same priority threads, this
will result in the target thread being scheduled. Return the amount of time consumed by this scheduling
context since the last timeout fault, <code class="language-plaintext highlighter-rouge">YieldTo</code> or <code class="language-plaintext highlighter-rouge">Consumed</code> invocation.</li>
  <li><code class="language-plaintext highlighter-rouge">seL4_SchedContext_Consumed</code> - Return the amount of time consumed by this scheduling
context since the last timeout fault, <code class="language-plaintext highlighter-rouge">YieldTo</code> or <code class="language-plaintext highlighter-rouge">Consumed</code> invocation.</li>
  <li><code class="language-plaintext highlighter-rouge">seL4_TCB_SetTimeoutEndpoint</code> - Set the timeout fault endpoint for a TCB.</li>
</ul>

<h3 id="reply-objects">Reply objects</h3>

<p>The MCS API also makes the reply channel explicit: reply capabilities are now fully fledged objects
which must be provided by a thread on <code class="language-plaintext highlighter-rouge">seL4_Recv</code> operations. They are used to track the scheduling
context donation chain and return donated scheduling contexts to callers.</p>

<p>Please see the <a href="https://docs.sel4.systems/sel4_release/seL4_9.0.0-mcs">release notes</a> and
<a href="https://docs.sel4.systems/sel4_release/seL4_9.0.0-mcs.html">manual</a> for further details
 on the API changes.</p>

<h2 id="exercises">Exercises</h2>

<p>In the initial state of the tutorial, the main function in <code class="language-plaintext highlighter-rouge">mcs.c</code> is running in one process, and the
following loop from <code class="language-plaintext highlighter-rouge">spinner.c</code> is running in another process:</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    int i = 0;
    while (1) {
        printf("Yield\n");
        seL4_Yield();
    }
</code></pre></div></div>

<p>Both processes share the same priority. The code in <code class="language-plaintext highlighter-rouge">mcs.c</code> binds
a scheduling context (<code class="language-plaintext highlighter-rouge">sched_context</code>) to the TCB of the spinner process (<code class="language-plaintext highlighter-rouge">spinner_tcb)</code> with round-robin scheduling parameters. As a result, you should see
 something like the following output, which continues uninterrupted:</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Yield
Yield
Yield
</code></pre></div></div>

<h3 id="periodic-threads">Periodic threads</h3>

<p><strong>Exercise</strong> Reconfigure <code class="language-plaintext highlighter-rouge">sched_context</code> with the following periodic scheduling parameters,
 (budget = <code class="language-plaintext highlighter-rouge">0.9 * US_IN_S</code>, period = <code class="language-plaintext highlighter-rouge">1 * US_IN_S</code>).</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">//TODO reconfigure sched_context to be periodic</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">// reconfigure sched_context to be periodic</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_SchedControl_Configure</span><span class="p">(</span><span class="n">sched_control</span><span class="p">,</span> <span class="n">sched_context</span><span class="p">,</span> <span class="mi">0</span><span class="p">.</span><span class="mi">9</span> <span class="o">*</span> <span class="n">US_IN_S</span><span class="p">,</span> <span class="mi">1</span> <span class="o">*</span> <span class="n">US_IN_S</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="mi">0</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span> <span class="o">!=</span> <span class="n">seL4_NoError</span><span class="p">,</span> <span class="s">"Failed to configure schedcontext"</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>By completing this task successfully, the output will not change, but the rate that the output is
printed will slow: each subsequent line should be output once the period has elapsed. You should now
be able to see the loop where the <code class="language-plaintext highlighter-rouge">mcs.c</code> process and <code class="language-plaintext highlighter-rouge">spinner.c</code> process alternate, until the <code class="language-plaintext highlighter-rouge">mcs.c</code>
process blocks, at which point <code class="language-plaintext highlighter-rouge">"Yield"</code> is emitted by <code class="language-plaintext highlighter-rouge">spinner.c</code> every second, as shown below:</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Yield
Tick 0
Yield
Tick 1
Yield
Tick 2
Yield
Tick 3
Yield
Tick 4
Yield
Tick 5
Yield
Tick 6
Yield
Tick 7
Yield
Tick 8
Yield
Yield
Yield
</code></pre></div></div>

<p>Before you completed this task, the scheduling context was round-robin, and so was
schedulable immediately after the call to <code class="language-plaintext highlighter-rouge">seL4_Yield</code>.
By changing
the scheduling parameters of <code class="language-plaintext highlighter-rouge">sched_context</code> to periodic parameters (budget &lt; period), each time
<code class="language-plaintext highlighter-rouge">seL4_Yield()</code> is called the available budget in the scheduling context is abandoned, causing the
thread to sleep until the next replenishment, determined by the period.</p>

<h3 id="unbinding-scheduling-contexts">Unbinding scheduling contexts</h3>

<p>You can cease a threads execution by unbinding the scheduling context.
Unlike <em>suspending</em> a thread via <code class="language-plaintext highlighter-rouge">seL4_TCB_Suspend</code>, unbinding will not change the thread state. Using suspend
cancels any system calls in process (e.g IPC) and renders the thread unschedulable by changing the
thread state. Unbinding a scheduling context does not alter the thread state, but merely removes the thread
from the scheduler queues.</p>

<p><strong>Exercise</strong> Unbind <code class="language-plaintext highlighter-rouge">sched_context</code> to stop the spinner process from running.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">//TODO unbind sched_context to stop yielding thread</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">// unbind sched_context to stop the yielding thread</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_SchedContext_Unbind</span><span class="p">(</span><span class="n">sched_context</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span><span class="p">,</span> <span class="s">"Failed to unbind sched_context"</span><span class="p">);</span>
</code></pre></div>  </div>

</details>

<p>On success, you should see the output from the yielding thread stop.</p>

<h3 id="sporadic-threads">Sporadic threads</h3>

<p>Your next task is to use a different process, <code class="language-plaintext highlighter-rouge">sender</code> to experiment with sporadic tasks. The
<code class="language-plaintext highlighter-rouge">sender</code> process is ready to run, and just needs a scheduling context in order to do so.</p>

<p><strong>Exercise</strong> First, bind <code class="language-plaintext highlighter-rouge">sched_context</code> to <code class="language-plaintext highlighter-rouge">sender_tcb</code>.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">//TODO bind sched_context to sender_tcb</span>
</code></pre></div></div>
<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">// bind sched_context to sender_tcb</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_SchedContext_Bind</span><span class="p">(</span><span class="n">sched_context</span><span class="p">,</span> <span class="n">sender_tcb</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span> <span class="o">!=</span> <span class="n">seL4_NoError</span><span class="p">,</span> <span class="s">"Failed to bind schedcontext"</span><span class="p">);</span>
</code></pre></div>  </div>

</details>

<p>The output should look like the following:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>...
Tock 3
Tock 4
Tock 5
Tock 6
</code></pre></div></div>

<p>Note the rate of the output: currently, you should see 2 lines come out at a time, with roughly
a second break between (the period of the scheduling context you set earlier). This is because
scheduling context only has the minimum sporadic refills (see background), and each time a context switch
occurs a refill is used up to schedule another.</p>

<p><strong>Exercise</strong> Reconfigure the <code class="language-plaintext highlighter-rouge">sched_context</code> to an extra 6 refills, such that all of the <code class="language-plaintext highlighter-rouge">Tock</code> output
occurs in one go.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">//TODO reconfigure sched_context to be periodic with 6 extra refills</span>
</code></pre></div></div>
<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">// reconfigure sched_context to be periodic with 6 extra refills</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_SchedControl_Configure</span><span class="p">(</span><span class="n">sched_control</span><span class="p">,</span> <span class="n">sched_context</span><span class="p">,</span> <span class="mi">0</span><span class="p">.</span><span class="mi">9</span> <span class="o">*</span> <span class="n">US_IN_S</span><span class="p">,</span> <span class="mi">1</span> <span class="o">*</span> <span class="n">US_IN_S</span><span class="p">,</span> <span class="mi">6</span><span class="p">,</span> <span class="mi">0</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span> <span class="o">!=</span> <span class="n">seL4_NoError</span><span class="p">,</span> <span class="s">"Failed to configure schedcontext"</span><span class="p">);</span>
</code></pre></div>  </div>

</details>

<h3 id="passive-servers-1">Passive servers</h3>

<p>Now look to the third process, <code class="language-plaintext highlighter-rouge">server.c</code>, which is a very basic echo server. It currently does
not have a scheduling context, and needs one to initialise.</p>

<p><strong>Exercise</strong> Bind <code class="language-plaintext highlighter-rouge">sched_context</code> to <code class="language-plaintext highlighter-rouge">server_tcb</code>.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">//TODO bind sched_context to server_tcb</span>
</code></pre></div></div>
<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">// bind the servers sched context</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_SchedContext_Bind</span><span class="p">(</span><span class="n">sched_context</span><span class="p">,</span> <span class="n">server_tcb</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span> <span class="o">!=</span> <span class="n">seL4_NoError</span><span class="p">,</span> <span class="s">"Failed to bind sched_context to server_tcb"</span><span class="p">);</span>
</code></pre></div>  </div>

</details>

<p>Now you should see the server initialise and echo the messages sent. Note the initialisation protocol:
first, you bound <code class="language-plaintext highlighter-rouge">sched_context</code> to the server. At this point, in <code class="language-plaintext highlighter-rouge">server.c</code>, the server calls
<code class="language-plaintext highlighter-rouge">seL4_NBSendRecv</code> which sends an IPC message on <code class="language-plaintext highlighter-rouge">endpoint</code>, indicating that the server is now initialised.
The output should be as follows</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Tock 8
Starting server
Wait for server
Server initialising
running
passive
echo server
Yield
</code></pre></div></div>

<p>The following code then converts the server to passive:</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">// convert to passive</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_SchedContext_Unbind</span><span class="p">(</span><span class="n">sched_context</span><span class="p">);</span>
</code></pre></div></div>

<p>From this point, the server runs on the <code class="language-plaintext highlighter-rouge">mcs</code> process’s scheduling context.</p>

<h3 id="timeout-faults-1">Timeout Faults</h3>

<p>But before we discuss timeout faults, we must first discuss the differences
between configuring a fault endpoint on the master vs the MCS kernel. There is a
minor difference in the way that the kernel is informed of the cap to a fault
endpoint, between the master and MCS kernels.</p>

<p>Regardless though, on both versions of the kernel, to inform the kernel of the
fault endpoint for a thread, call the usual <code class="language-plaintext highlighter-rouge">seL4_TCB_SetSpace()</code>.</p>

<h4 id="configuring-a-fault-endpoint-on-the-mcs-kernel">Configuring a fault endpoint on the MCS kernel:</h4>

<p>On the MCS kernel the cap given to the kernel must be a cap to an object in
the CSpace of the thread which is <em>calling the syscall</em> (<code class="language-plaintext highlighter-rouge">seL4_TCB_Configure()</code>)
to give the cap to the kernel.</p>

<p>This calling thread may be the handler thread, or some other thread which
manages both the handler thread and the faulting thread. Or in an oddly designed
system, it might be the faulting thread itself if the faulting thread is allowed
to configure its own fault endpoint.</p>

<p>The reason for this difference is merely that it is faster to lookup the fault
endpoint this way since it is looked up only once at the time it is configured.</p>

<h4 id="configuring-a-fault-endpoint-on-the-master-kernel">Configuring a fault endpoint on the Master kernel</h4>

<p>On the Master kernel the cap given to the kernel must be a cap to an object in
the CSpace of the <em>faulting thread</em>.</p>

<p>On the Master kernel, the fault endpoint cap is looked up from within the CSpace
of the faulting thread everytime a fault occurs.</p>

<h4 id="exercise">Exercise</h4>

<p><strong>Exercise</strong> Set the data field of <code class="language-plaintext highlighter-rouge">sched_context</code> using <code class="language-plaintext highlighter-rouge">seL4_SchedControl_Configure</code> and set a 10s period, 1ms
budget and 0 extra refills.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">//TODO reconfigure sched_context with 10s period, 1ms budget, 0 extra refills and data of 5.</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    <span class="c1">// reconfigure sched_context with 1s period, 500 microsecond budget, 0 extra refills and data of 5.</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_SchedControl_Configure</span><span class="p">(</span><span class="n">sched_control</span><span class="p">,</span> <span class="n">sched_context</span><span class="p">,</span> <span class="mi">500</span><span class="p">,</span> <span class="n">US_IN_S</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="mi">5</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span> <span class="o">!=</span> <span class="n">seL4_NoError</span><span class="p">,</span> <span class="s">"Failed to configure sched_context"</span><span class="p">);</span>
</code></pre></div>  </div>

</details>

<p>The code then binds the scheduling context back to <code class="language-plaintext highlighter-rouge">spinner_tcb</code>, which starts yielding again.</p>

<p><strong>Exercise</strong> set the timeout fault endpoint for <code class="language-plaintext highlighter-rouge">spinner_tcb</code>.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">//TODO set endpoint as the timeout fault handler for spinner_tcb</span>
</code></pre></div></div>
<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="c1">// set endpoint as the timeout fault handler for spinner_tcb</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_TCB_SetTimeoutEndpoint</span><span class="p">(</span><span class="n">spinner_tcb</span><span class="p">,</span> <span class="n">endpoint</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">error</span> <span class="o">!=</span> <span class="n">seL4_NoError</span><span class="p">,</span> <span class="s">"Failed to set timeout fault endpoint for spinner"</span><span class="p">);</span>
</code></pre></div>  </div>

</details>

<p>When the <code class="language-plaintext highlighter-rouge">spinner</code> faults, you should see the following output:</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Received timeout fault
Success!
</code></pre></div></div>

<h3 id="further-exercises">Further exercises</h3>

<p>That’s all for the detailed content of this tutorial. Below we list other ideas for exercises you can try,
to become more familiar with the MCS extensions.</p>

<ul>
  <li>Set up a passive server with a timeout fault handlers, with policies for clients that exhaust their budget.</li>
  <li>Experiment with notification binding on a passive server, by binding both a notification object to the
server TCB and an SC to the notification object.</li>
</ul>



<p style="text-align: right;">

      Next: <a href="/Tutorials/libraries-1">Initialisation &amp; threading</a>
</p>

<hr>
    <p><em>Tutorial included from <a href="https://github.com/sel4/sel4-tutorials/blob/master/tutorials/mcs/mcs.md">github repo</a> <a href="https://github.com/sel4/sel4-tutorials/edit/master/tutorials/mcs/mcs.md">edit</a></em></p>
  </div>

  
    
<div class="sidebar-toc hidden-xs hidden-sm col-md-3 col-lg-3">
    <ul id="toc" class="section-nav">
<li class="toc-entry toc-h2"><a href="#prerequisites">Prerequisites</a></li>
<li class="toc-entry toc-h2"><a href="#initialising">Initialising</a></li>
<li class="toc-entry toc-h2"><a href="#background">Background</a>
<ul>
<li class="toc-entry toc-h3"><a href="#scheduling-contexts">Scheduling Contexts</a></li>
<li class="toc-entry toc-h3"><a href="#schedcontrol">SchedControl</a></li>
<li class="toc-entry toc-h3"><a href="#schedcontext-binding">SchedContext Binding</a></li>
<li class="toc-entry toc-h3"><a href="#bounding-execution">Bounding execution</a></li>
<li class="toc-entry toc-h3"><a href="#scheduler">Scheduler</a></li>
<li class="toc-entry toc-h3"><a href="#passive-servers">Passive servers</a></li>
<li class="toc-entry toc-h3"><a href="#timeout-faults">Timeout faults</a></li>
<li class="toc-entry toc-h3"><a href="#new-invocations">New invocations</a></li>
<li class="toc-entry toc-h3"><a href="#reply-objects">Reply objects</a></li>
</ul>
</li>
<li class="toc-entry toc-h2"><a href="#exercises">Exercises</a>
<ul>
<li class="toc-entry toc-h3"><a href="#periodic-threads">Periodic threads</a></li>
<li class="toc-entry toc-h3"><a href="#unbinding-scheduling-contexts">Unbinding scheduling contexts</a></li>
<li class="toc-entry toc-h3"><a href="#sporadic-threads">Sporadic threads</a></li>
<li class="toc-entry toc-h3"><a href="#passive-servers-1">Passive servers</a></li>
<li class="toc-entry toc-h3"><a href="#timeout-faults-1">Timeout Faults</a>
<ul>
<li class="toc-entry toc-h4"><a href="#configuring-a-fault-endpoint-on-the-mcs-kernel">Configuring a fault endpoint on the MCS kernel:</a></li>
<li class="toc-entry toc-h4"><a href="#configuring-a-fault-endpoint-on-the-master-kernel">Configuring a fault endpoint on the Master kernel</a></li>
<li class="toc-entry toc-h4"><a href="#exercise">Exercise</a></li>
</ul>
</li>
<li class="toc-entry toc-h3"><a href="#further-exercises">Further exercises</a></li>
</ul>
</li>
</ul>
</div>

  
</div>
<script src="/assets/js/toggle-markdown.js"></script>

    </main>
    


<footer class="site-footer">

  <h2 class="footer-heading">seL4 docs</h2>

  <div class="footer-col-wrapper">

    <div class="col-md-2">
      



<ul class="social-media-list">
  <li><a href="https://github.com/sel4"><i class="fab fa-github"></i> <span class="username">sel4</span></a></li><li><a href="https://github.com/sel4proj"><i class="fab fa-github"></i> <span class="username">sel4proj</span></a></li>
</ul>

    </div>

    <div class="col-md-8">
      <ul class="list-unstyled">
        <li>
          This site is for displaying seL4 related documentation.  Pull requests are welcome.
        </li>
        
          <li>
            Site last updated: Fri Feb 7 10:17:38 2025 +1100 ee78c8857c
          </li>
          <li>
                Page last updated: Mon Jan 6 18:52:01 2025 +1100 df31e5ccb8
          </li>
        
      </ul>
    </div>
    <div class="col-md-2">
<a href="https://github.com/seL4/docs/blob/master/Tutorials/mcs.md">View page on GitHub</a>
      <br />
      <a href="https://github.com/seL4/docs/edit/master/Tutorials/mcs.md">Edit page on GitHub</a>
      <br />
      <a href="/sitemap">Sitemap</a>
    </div>

  </div>

</footer>

  </body>
</html>
